$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$), $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$).
\\[0ex]single{-}thread{-}generator\{i:l\}(${\it es}$;$P$;$R$)
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:E. ($R$($e$,${\it e'}$)) $\Rightarrow$ ($P$($e$) \& $P$(${\it e'}$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$, $b$, $e$:E. ($R$($a$,$e$) \& $R$($b$,$e$)) $\Rightarrow$ ($P$($e$) \& $P$($a$) \& $P$($b$)) $\Rightarrow$ ($a$ = $b$))